$\forall$$i$:Id. R{-}Feasible\{i:l\}(onceR\{a:ut2, done:ut2\}($i$))